The classic Boolean satisfiability problem can be generally stated as follows: for a given Boolean function of variables, determine whether it is possible to assign values to the variables such that the function is satisfied (that is, the function evaluates to true), or whether no such assignment exists. The Boolean satisfiability problem is of significance in both theoretical research and in practical applications such as artificial intelligence planning, circuit testing, software verification, and database validation.
The satisfiability problem can be solved by representing the Boolean function as a directed acyclic graph (DAG), where each vertex of the DAG represents a variable assignment with the exception of two sink nodes. One sink node represents false function results (e.g., binary zero) and the other sink node represents true function results (e.g., binary one). Each vertex of the DAG likewise has a binary domain. Generally speaking, the function is satisfiable if there is a path through the DAG from a root node to the “one” sink (the true node).
The amount of time and resources needed to determine satisfiability of a function using a DAG such as that just described increases as the number of variables in the function increases. A more efficient approach that saves time and resources would be valuable.